(assert (forall ((a Int) (b Int)) (xor (xor (= a 0) (= b 0)) (forall ((c Int)) (= (ite (= a 0) 0 1) (ite (= c 0) 0 1))))))
(check-sat)
